\begin{tabbing}
$\forall$\=$T$:Type$_{\mbox{\scriptsize i}}$, $L$:$T$ List, $R$:(\{$x$:$T$$\mid$ ($x$ $\in$ $L$) \}$\rightarrow$es\_realizer\{i:l\}),\+
\\[0ex]$P$:(\{$x$:$T$$\mid$ ($x$ $\in$ $L$) \}$\rightarrow$ES\{i\}$\rightarrow$Prop$_{\mbox{\scriptsize i'}}$).
\-\\[0ex]($\forall$$x$, $y$:$T$. Dec($x$ $=$ $y$))
\\[0ex]$\Rightarrow$ ($\forall$$x$$\in$$L$. $R$($x$) $\Vdash$\{i\} ${\it es}$.$P$($x$,${\it es}$))
\\[0ex]$\Rightarrow$ ($\forall$$x$$\in$$L$. $\forall$$y$$\in$$L$. $\neg$$x$ $=$ $y$ $\in$ $T$ $\Rightarrow$ R{-}compat\{i:l\}($R$($x$); $R$($y$)))
\\[0ex]$\Rightarrow$ $\oplus$$x$$\in$$L$.$R$($x$) $\Vdash$\{i\} ${\it es}$.$\forall$$x$$\in$$L$. $P$($x$,${\it es}$)
\end{tabbing}